p(0(x1)) → s(s(0(s(s(p(x1))))))
p(s(0(x1))) → 0(x1)
p(s(s(x1))) → s(p(s(x1)))
f(s(x1)) → g(q(i(x1)))
g(x1) → f(p(p(x1)))
q(i(x1)) → q(s(x1))
q(s(x1)) → s(s(x1))
i(x1) → s(x1)
↳ QTRS
↳ DependencyPairsProof
p(0(x1)) → s(s(0(s(s(p(x1))))))
p(s(0(x1))) → 0(x1)
p(s(s(x1))) → s(p(s(x1)))
f(s(x1)) → g(q(i(x1)))
g(x1) → f(p(p(x1)))
q(i(x1)) → q(s(x1))
q(s(x1)) → s(s(x1))
i(x1) → s(x1)
F(s(x1)) → G(q(i(x1)))
G(x1) → P(x1)
P(0(x1)) → P(x1)
F(s(x1)) → Q(i(x1))
Q(i(x1)) → Q(s(x1))
G(x1) → F(p(p(x1)))
F(s(x1)) → I(x1)
P(s(s(x1))) → P(s(x1))
G(x1) → P(p(x1))
p(0(x1)) → s(s(0(s(s(p(x1))))))
p(s(0(x1))) → 0(x1)
p(s(s(x1))) → s(p(s(x1)))
f(s(x1)) → g(q(i(x1)))
g(x1) → f(p(p(x1)))
q(i(x1)) → q(s(x1))
q(s(x1)) → s(s(x1))
i(x1) → s(x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
F(s(x1)) → G(q(i(x1)))
G(x1) → P(x1)
P(0(x1)) → P(x1)
F(s(x1)) → Q(i(x1))
Q(i(x1)) → Q(s(x1))
G(x1) → F(p(p(x1)))
F(s(x1)) → I(x1)
P(s(s(x1))) → P(s(x1))
G(x1) → P(p(x1))
p(0(x1)) → s(s(0(s(s(p(x1))))))
p(s(0(x1))) → 0(x1)
p(s(s(x1))) → s(p(s(x1)))
f(s(x1)) → g(q(i(x1)))
g(x1) → f(p(p(x1)))
q(i(x1)) → q(s(x1))
q(s(x1)) → s(s(x1))
i(x1) → s(x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ QDP
P(s(s(x1))) → P(s(x1))
p(0(x1)) → s(s(0(s(s(p(x1))))))
p(s(0(x1))) → 0(x1)
p(s(s(x1))) → s(p(s(x1)))
f(s(x1)) → g(q(i(x1)))
g(x1) → f(p(p(x1)))
q(i(x1)) → q(s(x1))
q(s(x1)) → s(s(x1))
i(x1) → s(x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P(s(s(x1))) → P(s(x1))
The value of delta used in the strict ordering is 1.
POL(P(x1)) = (2)x_1
POL(s(x1)) = 1/4 + (2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
↳ QDP
p(0(x1)) → s(s(0(s(s(p(x1))))))
p(s(0(x1))) → 0(x1)
p(s(s(x1))) → s(p(s(x1)))
f(s(x1)) → g(q(i(x1)))
g(x1) → f(p(p(x1)))
q(i(x1)) → q(s(x1))
q(s(x1)) → s(s(x1))
i(x1) → s(x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
P(0(x1)) → P(x1)
p(0(x1)) → s(s(0(s(s(p(x1))))))
p(s(0(x1))) → 0(x1)
p(s(s(x1))) → s(p(s(x1)))
f(s(x1)) → g(q(i(x1)))
g(x1) → f(p(p(x1)))
q(i(x1)) → q(s(x1))
q(s(x1)) → s(s(x1))
i(x1) → s(x1)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
P(0(x1)) → P(x1)
The value of delta used in the strict ordering is 1/2.
POL(P(x1)) = (2)x_1
POL(0(x1)) = 1/4 + (7/2)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
p(0(x1)) → s(s(0(s(s(p(x1))))))
p(s(0(x1))) → 0(x1)
p(s(s(x1))) → s(p(s(x1)))
f(s(x1)) → g(q(i(x1)))
g(x1) → f(p(p(x1)))
q(i(x1)) → q(s(x1))
q(s(x1)) → s(s(x1))
i(x1) → s(x1)
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDP
F(s(x1)) → G(q(i(x1)))
G(x1) → F(p(p(x1)))
p(0(x1)) → s(s(0(s(s(p(x1))))))
p(s(0(x1))) → 0(x1)
p(s(s(x1))) → s(p(s(x1)))
f(s(x1)) → g(q(i(x1)))
g(x1) → f(p(p(x1)))
q(i(x1)) → q(s(x1))
q(s(x1)) → s(s(x1))
i(x1) → s(x1)